Search for: All records

In high-level design explorations, many useful optimizations transform a circuit into another with different operating cycles for a better trade-off between performance and resource usage. How to efficiently check their equivalence is critical and challenging since most existing equivalence checkers are designed for cycle-accurate circuits. This paper presents SE3, an efficient sequential equivalence checker without assumption on cycle-accuracy, latch mapping, or I/O interface of the checked circuits. It proves the equivalence of two circuits by computing an equivalence relation between the states of the two circuits and utilizes syntax abstraction to accelerate this process. Experimental results show that SE3 is significantly faster than state-of-the-art sequential equivalence checking algorithms. 

With the rapid evolution of the IC supply chain, circuit IP protection has become a critical realistic issue for the semiconductor industry. One promising technique to resolve the issue is logic locking. It adds key inputs to the original circuit such that only authorized users can get the correct function, and it modifies the circuit to obfuscate it against structural analysis. However, there is a trilemma among locking, obfuscation, and efficiency within all existing logic locking methods that at most two of the objectives can be achieved. In this work, we propose ObfusLock, the first logic locking method that simultaneously achieves all three objectives: locking security, obfuscation safety, and locking efficiency. ObfusLock is based on solid mathematical proofs, incurs small overheads (<5% on average), and has passed experimental tests of various existing attacks. 

In recent years, semiconductor industry has out-sourced the manufacturing to low-cost but not necessarily trusted foundries. This fabless business model encounters new security challenges, including piracy and overproduction. A well-studied solution to prevent unauthorized products from functioning is logic encryption, where a chip is encrypted using a key only known to the designer. However, the majority of the logic encryption solutions are vulnerable due to key uniformity and probing attacks. In this paper, we first present GSAT, a Global attack on existing IC-specific logic encryption schemes using the SAT model, that effectively deciphers the hidden global key pluggable to all the encrypted ICs. Next, we propose a highly secure and low-cost remedy called SPLEnD: Strong PUF -based Logic Encryption Design. Traditional I C-specific encryption schemes are vulnerable to GSAT attack, while SPLEnD not only effectively resists GSAT, but also balances security and efficiency. 

The active participation of external entities in the manufacturing flow has produced numerous hardware security issues in which piracy and overproduction are likely to be the most ubiquitous and expensive ones. The main approach to prevent unauthorized products from functioning is logic encryption that inserts key-controlled gates to the original circuit in a way that the valid behavior of the circuit only happens when the correct key is applied. The challenge for the security designer is to ensure neither the correct key nor the original circuit can be revealed by different analyses of the encrypted circuit. However, in state-of-the-art logic encryption works, a lot of performance is sold to guarantee security against powerful logic and structural attacks. This contradicts the primary reason of logic encryption that is to protect a precious design from being pirated and overproduced. In this paper, we propose a bilateral logic encryption platform that maintains high degree of security with small circuit modification. The robustness against exact and approximate attacks is also demonstrated. 

Logic encryption, a method to lock a circuit from unauthorized use unless the correct key is provided, is the most important technique in hardware IP protection. However, with the discovery of the SAT attack, all traditional logic encryption algorithms are broken. New algorithms after the SAT attack are all vulnerable to structural analysis unless a provable obfuscation is applied to the locked circuit. But there is no provable logic obfuscation available, in spite of some vague resorting to logic resynthesis. In this paper, we formulate and discuss a trilemma in logic encryption among locking robustness, structural security, and encryption efficiency, showing that pre-SAT approaches achieve only structural security and encryption efficiency, and post-SAT approaches achieve only locking robustness and encryption efficiency. There is also a dilemma between query complexity and error number in locking. We first develop a theory and solution to the dilemma in locking between query complexity and error number. Then, we provide a provable obfuscation solution to the dilemma between structural security and locking robustness. We finally present and discuss some results towards the resolution of the trilemma in logic encryption. 

Logic encryption is a powerful hardware protection technique that uses extra key inputs to lock a circuit from piracy or unauthorized use. The recent discovery of the SAT-based attack with Distinguishing Input Pattern (DIP) generation has rendered all traditional logic encryptions vulnerable, and thus the creation of new encryption methods. However, a critical question for any new encryption method is whether security against the DIP-generation attack means security against all other attacks. In this paper, a new high-level SAT-based attack called SigAttack has been discovered and thoroughly investigated. It is based on extracting a key-revealing signature in the encryption. A majority of all known SAT-resilient encryptions are shown to be vulnerable to SigAttack. By formulating the condition under which SigAttack is effective, the paper also provides guidance for the future logic encryption design.